Java Modeling Language
part 4/8 · 12.1 KB total
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Defines a JML assertion.
spec_public
Declares a protected or private variable public for specification purposes.
Basic JML also provides the following expressions
\result
An identifier for the return value of the method that follows.
\old(<expression>)
A modifier to refer to the value of the <expression> at the time of entry into a method.
(\forall <decl>; <range-exp>; <body-exp>)
The universal quantifier.
(\exists <decl>; <range-exp>; <body-exp>)
a ==> b
a implies b
a <== b
a is implied by b
a <==> b
a if and only if b
as well as standard Java syntax for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like
public class BankingExample
{
public static final int MAX_BALANCE = 1000;
private /*@ spec_public @*/ int balance;
private /*@ spec_public @*/ boolean isLocked = false;
//@ public invariant balance >= 0 && balance <= MAX_BALANCE;
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────